!!! Поправка к файлам в решении:
    У меня uppaal не сохраняет queries в файл, т.к. падает, поэтому мои queries сохранены xml файл.
    (так же они объяснены и продублированны ниже)
    Однако я добавил 2 файла - трассы, которые имеют минимальную длинну расписания (их можно открыть в uppaal)
    
    Ещё я поджал количество состояний в модели 3_3 - по сравнению с моделью 3_1, что сильно помогло в подсчёте через verifyta, я обозвал файлы 3_3u - приложил к ответу (хотя это и не помогло запустить 3 на 9, хоть и пытался)

Поведение verifyta (количество требуемых ресурсов) (время для одного ядра моего процессора - 2,4ГГц):
    Для первых 6 процессов - работает нормально и достаточно быстро (меньше минуты)
    Для первых 7 процессов - работает нормально, но достаточно долго (минут 5) (требует достаточно много памяти - где-то 3-4 гига оперативной памяти)
    Для первых 8, 9 процессов - ему не хватает даже 5 гигов памяти, он их выедает и падает

В связи с проблемами с возможностями аппараруты моё задание было переформулированно и вместо 3-х процессоров, я работаю на 2-х.

Особенность моей модели:
    Дело в том, что если verifyta попросить выдать мне самую короткую трассу (в моей модели), то автоматически это будет та трасса, которая выполняется быстрее всего, т.е. мне автоматически выдадут после прогона трассу, в которой самое быстрое выполнение.
    (Если поставить Options->DiagnosticTrace->Shortest)
    
    Поэтому для вычисления в верификации я испольховал выражение:
    E<> (solvedJobs[1]==1 && solvedJobs[2]==1 && solvedJobs[3]==1 && solvedJobs[4]==1 && solvedJobs[5]==1 && solvedJobs[6]==1 && solvedJobs[7]==1 && solvedJobs[8]==1 && solvedJobs[9]==1)
    Вместе с просьбой uppaal выдать самую короткую трассу - даст нужную трассу, если вы считаете минимальное время

Проверка свойств:
    Для того, чтобы проверить, что все работы выполняются при всех возможных комбинациях:
    E<> (solvedJobs[1]==1 && solvedJobs[2]==1 && solvedJobs[3]==1 && solvedJobs[4]==1 && solvedJobs[5]==1 && solvedJobs[6]==1 && solvedJobs[7]==1 && solvedJobs[8]==1 && solvedJobs[9]==1)
    Т.е. всегда для любой трассы найдётся состояние, в котором все задачи будут выполнены (это правило совпадает с правилом выше)
    (моя модель построена так, что после выполнения всех задач - она останавливается)

    Для того, чтобы угадывать время, при котором всё ещё есть трасса, на которой выполняется свойство:
    E<> (time > 40 && (solvedJobs[1]==1 && solvedJobs[2]==1 && solvedJobs[3]==1 && solvedJobs[4]==1 && solvedJobs[5]==1 && solvedJobs[6]==1 && solvedJobs[7]==1 && solvedJobs[8]==1 && solvedJobs[9]==1))
    (т.е. на любом пути существует событие, когда все задачи уже выполнены, а время больше 40, тогда если пороговое значение 40 - минимальная трасса, то для неё это свойство не будет выполняться, и тогда verifyta выдаст нам not satisfied, в то время, как для 41 - выдаст satisfied, что и будет значить, что 40 - наш порог)
    (но я буду использовать особенность моей модели, описанную выше для получения минимального времени и трассы сразу)

пункт 2 (потребовал около 2-х гигов памяти):
    Видел что при случайном симулировании в симуляторе - можно выполнить за 33 шага процессора.
    Проверка свойств описана выше - свойства выполнены
    
    Самое быстрое - 24 тика.
    Пример трассы:
           012345678901234567890123
    cpu0 - BCCCCCCCC FFFFFFFFFFFFFF
    cpu1 - AAEI     DGGGGGGGGGGHH
    
    При различных способах обхода дерева -  в глубину и в ширину:
        Т.к. нужно проверить свойство для каждой трассы - то приходится всё равно перебирать все возможные варианты, и потому скорость не сильно меняется, но важно количество используемой памяти - в случае, когда используется обход в глубину используется меньшее количество памяти, что важно.

пункт 4:
    Момент времени отказа - 15
    Видел что при случайном симулировании в симуляторе - можно выполнить за 31 шага процессора.
    Проверка свойств описана выше
    
    Самое быстрое - 28 тиков.
    Пример трассы:
           0123456789012345678901234567
    cpu0 - BCCCCCCCC FFFFF FFFFFFFFFFFF
    cpu1 - AAEI     DGGGGGGGGGGHH
    Замечу, что тут нумерация следующая:
        с нуля
        ошибка на процессоре происходит после момента отказа (поэтому в качестве момента отказа я в модели указал 14)
    
    При различных способах обхода дерева -  в глубину и в ширину:
        Т.к. нужно проверить свойство для каждой трассы - то приходится всё равно перебирать все возможные варианты, и потому скорость не сильно меняется, но важно количество используемой памяти - в случае, когда используется обход в глубину используется меньшее количество памяти, что важно.

Возможности UPPAAL:
    1) автоматизации несколько не хватает, для сбора всякого рода статистики, ...
    2) Мощное, но постоянно что-то там падает (мне приходилось стыковать verifyta на винтуальном линуксе с работой java под windows)
    3) Для больших моделей - быстро растёт количество комбинаций и в итоге не хватает памяти для проверки свойств модели